YES 1.6440000000000001
H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/empty.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:
↳ HASKELL
↳ BR
mainModule Main
| ((notElem :: (Eq b, Eq a) => (b,a) -> [(b,a)] -> Bool) :: (Eq b, Eq a) => (b,a) -> [(b,a)] -> Bool) |
module Main where
Replaced joker patterns by fresh variables and removed binding patterns.
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
mainModule Main
| ((notElem :: (Eq a, Eq b) => (a,b) -> [(a,b)] -> Bool) :: (Eq a, Eq b) => (a,b) -> [(a,b)] -> Bool) |
module Main where
Cond Reductions:
The following Function with conditions
is transformed to
undefined0 | True | = undefined |
undefined1 | | = undefined0 False |
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
mainModule Main
| (notElem :: (Eq b, Eq a) => (a,b) -> [(a,b)] -> Bool) |
module Main where
Haskell To QDPs
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_primPlusNat(Succ(xv3400), Succ(xv4001000)) → new_primPlusNat(xv3400, xv4001000)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primPlusNat(Succ(xv3400), Succ(xv4001000)) → new_primPlusNat(xv3400, xv4001000)
The graph contains the following edges 1 > 1, 2 > 2
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_primMulNat(Succ(xv30100), Succ(xv400100)) → new_primMulNat(xv30100, Succ(xv400100))
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primMulNat(Succ(xv30100), Succ(xv400100)) → new_primMulNat(xv30100, Succ(xv400100))
The graph contains the following edges 1 > 1, 2 >= 2
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_primEqNat(Succ(xv3000), Succ(xv40000)) → new_primEqNat(xv3000, xv40000)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primEqNat(Succ(xv3000), Succ(xv40000)) → new_primEqNat(xv3000, xv40000)
The graph contains the following edges 1 > 1, 2 > 2
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_esEs(@2(xv30, xv31), @2(xv400, xv401), app(app(ty_@2, ba), bb), bc) → new_esEs(xv30, xv400, ba, bb)
new_esEs(@2(@3(xv300, xv301, xv302), xv31), @2(@3(xv4000, xv4001, xv4002), xv401), app(app(app(ty_@3, hh), gg), app(ty_Maybe, bbd)), bc) → new_esEs0(xv302, xv4002, bbd)
new_esEs(@2(@3(xv300, xv301, xv302), xv31), @2(@3(xv4000, xv4001, xv4002), xv401), app(app(app(ty_@3, app(app(ty_Either, hb), hc)), gg), gh), bc) → new_esEs1(xv300, xv4000, hb, hc)
new_esEs(@2(@3(xv300, xv301, xv302), xv31), @2(@3(xv4000, xv4001, xv4002), xv401), app(app(app(ty_@3, hh), app(app(ty_Either, bad), bae)), gh), bc) → new_esEs1(xv301, xv4001, bad, bae)
new_esEs3(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), hh, gg, app(app(ty_@2, bbb), bbc)) → new_esEs(xv302, xv4002, bbb, bbc)
new_esEs1(Right(xv300), Right(xv4000), dh, app(ty_Maybe, ec)) → new_esEs0(xv300, xv4000, ec)
new_esEs(@2(xv30, xv31), @2(xv400, xv401), bcc, app(ty_[], bda)) → new_esEs2(xv31, xv401, bda)
new_esEs(@2(Right(xv300), xv31), @2(Right(xv4000), xv401), app(app(ty_Either, dh), app(app(ty_Either, ed), ee)), bc) → new_esEs1(xv300, xv4000, ed, ee)
new_esEs3(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), hh, app(ty_Maybe, bac), gh) → new_esEs0(xv301, xv4001, bac)
new_esEs(@2(@3(xv300, xv301, xv302), xv31), @2(@3(xv4000, xv4001, xv4002), xv401), app(app(app(ty_@3, hh), gg), app(app(app(ty_@3, bbh), bca), bcb)), bc) → new_esEs3(xv302, xv4002, bbh, bca, bcb)
new_esEs(@2(@3(xv300, xv301, xv302), xv31), @2(@3(xv4000, xv4001, xv4002), xv401), app(app(app(ty_@3, app(ty_[], hd)), gg), gh), bc) → new_esEs2(xv300, xv4000, hd)
new_esEs(@2(:(xv300, xv301), xv31), @2(:(xv4000, xv4001), xv401), app(ty_[], app(ty_Maybe, fd)), bc) → new_esEs0(xv300, xv4000, fd)
new_esEs(@2(@3(xv300, xv301, xv302), xv31), @2(@3(xv4000, xv4001, xv4002), xv401), app(app(app(ty_@3, app(app(app(ty_@3, he), hf), hg)), gg), gh), bc) → new_esEs3(xv300, xv4000, he, hf, hg)
new_esEs(@2(@3(xv300, xv301, xv302), xv31), @2(@3(xv4000, xv4001, xv4002), xv401), app(app(app(ty_@3, app(app(ty_@2, ge), gf)), gg), gh), bc) → new_esEs(xv300, xv4000, ge, gf)
new_esEs(@2(@3(xv300, xv301, xv302), xv31), @2(@3(xv4000, xv4001, xv4002), xv401), app(app(app(ty_@3, hh), app(app(app(ty_@3, bag), bah), bba)), gh), bc) → new_esEs3(xv301, xv4001, bag, bah, bba)
new_esEs0(Just(xv300), Just(xv4000), app(ty_Maybe, bf)) → new_esEs0(xv300, xv4000, bf)
new_esEs3(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), app(ty_[], hd), gg, gh) → new_esEs2(xv300, xv4000, hd)
new_esEs3(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), hh, gg, app(ty_Maybe, bbd)) → new_esEs0(xv302, xv4002, bbd)
new_esEs1(Left(xv300), Left(xv4000), app(app(ty_Either, db), dc), cg) → new_esEs1(xv300, xv4000, db, dc)
new_esEs(@2(@3(xv300, xv301, xv302), xv31), @2(@3(xv4000, xv4001, xv4002), xv401), app(app(app(ty_@3, hh), app(ty_[], baf)), gh), bc) → new_esEs2(xv301, xv4001, baf)
new_esEs3(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), app(app(ty_Either, hb), hc), gg, gh) → new_esEs1(xv300, xv4000, hb, hc)
new_esEs(@2(Just(xv300), xv31), @2(Just(xv4000), xv401), app(ty_Maybe, app(app(ty_@2, bd), be)), bc) → new_esEs(xv300, xv4000, bd, be)
new_esEs2(:(xv300, xv301), :(xv4000, xv4001), app(ty_Maybe, fd)) → new_esEs0(xv300, xv4000, fd)
new_esEs3(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), hh, app(app(ty_Either, bad), bae), gh) → new_esEs1(xv301, xv4001, bad, bae)
new_esEs0(Just(xv300), Just(xv4000), app(app(app(ty_@3, cb), cc), cd)) → new_esEs3(xv300, xv4000, cb, cc, cd)
new_esEs(@2(@3(xv300, xv301, xv302), xv31), @2(@3(xv4000, xv4001, xv4002), xv401), app(app(app(ty_@3, hh), gg), app(ty_[], bbg)), bc) → new_esEs2(xv302, xv4002, bbg)
new_esEs1(Right(xv300), Right(xv4000), dh, app(app(ty_@2, ea), eb)) → new_esEs(xv300, xv4000, ea, eb)
new_esEs(@2(xv30, xv31), @2(xv400, xv401), bcc, app(app(ty_Either, bcg), bch)) → new_esEs1(xv31, xv401, bcg, bch)
new_esEs(@2(xv30, xv31), @2(xv400, xv401), bcc, app(app(app(ty_@3, bdb), bdc), bdd)) → new_esEs3(xv31, xv401, bdb, bdc, bdd)
new_esEs(@2(Right(xv300), xv31), @2(Right(xv4000), xv401), app(app(ty_Either, dh), app(ty_Maybe, ec)), bc) → new_esEs0(xv300, xv4000, ec)
new_esEs3(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), app(ty_Maybe, ha), gg, gh) → new_esEs0(xv300, xv4000, ha)
new_esEs2(:(xv300, xv301), :(xv4000, xv4001), app(ty_[], fh)) → new_esEs2(xv300, xv4000, fh)
new_esEs(@2(Right(xv300), xv31), @2(Right(xv4000), xv401), app(app(ty_Either, dh), app(app(ty_@2, ea), eb)), bc) → new_esEs(xv300, xv4000, ea, eb)
new_esEs(@2(xv30, xv31), @2(xv400, xv401), bcc, app(app(ty_@2, bcd), bce)) → new_esEs(xv31, xv401, bcd, bce)
new_esEs(@2(@3(xv300, xv301, xv302), xv31), @2(@3(xv4000, xv4001, xv4002), xv401), app(app(app(ty_@3, hh), app(ty_Maybe, bac)), gh), bc) → new_esEs0(xv301, xv4001, bac)
new_esEs3(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), hh, gg, app(ty_[], bbg)) → new_esEs2(xv302, xv4002, bbg)
new_esEs(@2(@3(xv300, xv301, xv302), xv31), @2(@3(xv4000, xv4001, xv4002), xv401), app(app(app(ty_@3, hh), gg), app(app(ty_Either, bbe), bbf)), bc) → new_esEs1(xv302, xv4002, bbe, bbf)
new_esEs1(Left(xv300), Left(xv4000), app(app(ty_@2, ce), cf), cg) → new_esEs(xv300, xv4000, ce, cf)
new_esEs(@2(:(xv300, xv301), xv31), @2(:(xv4000, xv4001), xv401), app(ty_[], app(app(app(ty_@3, ga), gb), gc)), bc) → new_esEs3(xv300, xv4000, ga, gb, gc)
new_esEs(@2(Left(xv300), xv31), @2(Left(xv4000), xv401), app(app(ty_Either, app(app(ty_@2, ce), cf)), cg), bc) → new_esEs(xv300, xv4000, ce, cf)
new_esEs0(Just(xv300), Just(xv4000), app(ty_[], ca)) → new_esEs2(xv300, xv4000, ca)
new_esEs3(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), hh, gg, app(app(app(ty_@3, bbh), bca), bcb)) → new_esEs3(xv302, xv4002, bbh, bca, bcb)
new_esEs3(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), hh, app(app(ty_@2, baa), bab), gh) → new_esEs(xv301, xv4001, baa, bab)
new_esEs1(Left(xv300), Left(xv4000), app(ty_[], dd), cg) → new_esEs2(xv300, xv4000, dd)
new_esEs(@2(@3(xv300, xv301, xv302), xv31), @2(@3(xv4000, xv4001, xv4002), xv401), app(app(app(ty_@3, hh), app(app(ty_@2, baa), bab)), gh), bc) → new_esEs(xv301, xv4001, baa, bab)
new_esEs(@2(@3(xv300, xv301, xv302), xv31), @2(@3(xv4000, xv4001, xv4002), xv401), app(app(app(ty_@3, hh), gg), app(app(ty_@2, bbb), bbc)), bc) → new_esEs(xv302, xv4002, bbb, bbc)
new_esEs3(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), app(app(ty_@2, ge), gf), gg, gh) → new_esEs(xv300, xv4000, ge, gf)
new_esEs(@2(:(xv300, xv301), xv31), @2(:(xv4000, xv4001), xv401), app(ty_[], app(app(ty_Either, ff), fg)), bc) → new_esEs1(xv300, xv4000, ff, fg)
new_esEs(@2(@3(xv300, xv301, xv302), xv31), @2(@3(xv4000, xv4001, xv4002), xv401), app(app(app(ty_@3, app(ty_Maybe, ha)), gg), gh), bc) → new_esEs0(xv300, xv4000, ha)
new_esEs(@2(Just(xv300), xv31), @2(Just(xv4000), xv401), app(ty_Maybe, app(app(app(ty_@3, cb), cc), cd)), bc) → new_esEs3(xv300, xv4000, cb, cc, cd)
new_esEs(@2(xv30, xv31), @2(xv400, xv401), bcc, app(ty_Maybe, bcf)) → new_esEs0(xv31, xv401, bcf)
new_esEs1(Right(xv300), Right(xv4000), dh, app(app(ty_Either, ed), ee)) → new_esEs1(xv300, xv4000, ed, ee)
new_esEs(@2(Just(xv300), xv31), @2(Just(xv4000), xv401), app(ty_Maybe, app(app(ty_Either, bg), bh)), bc) → new_esEs1(xv300, xv4000, bg, bh)
new_esEs(@2(Left(xv300), xv31), @2(Left(xv4000), xv401), app(app(ty_Either, app(ty_[], dd)), cg), bc) → new_esEs2(xv300, xv4000, dd)
new_esEs(@2(:(xv300, xv301), xv31), @2(:(xv4000, xv4001), xv401), app(ty_[], app(app(ty_@2, fb), fc)), bc) → new_esEs(xv300, xv4000, fb, fc)
new_esEs1(Left(xv300), Left(xv4000), app(ty_Maybe, da), cg) → new_esEs0(xv300, xv4000, da)
new_esEs(@2(Left(xv300), xv31), @2(Left(xv4000), xv401), app(app(ty_Either, app(app(app(ty_@3, de), df), dg)), cg), bc) → new_esEs3(xv300, xv4000, de, df, dg)
new_esEs3(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), hh, app(app(app(ty_@3, bag), bah), bba), gh) → new_esEs3(xv301, xv4001, bag, bah, bba)
new_esEs0(Just(xv300), Just(xv4000), app(app(ty_@2, bd), be)) → new_esEs(xv300, xv4000, bd, be)
new_esEs(@2(Just(xv300), xv31), @2(Just(xv4000), xv401), app(ty_Maybe, app(ty_Maybe, bf)), bc) → new_esEs0(xv300, xv4000, bf)
new_esEs(@2(Left(xv300), xv31), @2(Left(xv4000), xv401), app(app(ty_Either, app(app(ty_Either, db), dc)), cg), bc) → new_esEs1(xv300, xv4000, db, dc)
new_esEs0(Just(xv300), Just(xv4000), app(app(ty_Either, bg), bh)) → new_esEs1(xv300, xv4000, bg, bh)
new_esEs(@2(:(xv300, xv301), xv31), @2(:(xv4000, xv4001), xv401), app(ty_[], gd), bc) → new_esEs2(xv301, xv4001, gd)
new_esEs1(Right(xv300), Right(xv4000), dh, app(app(app(ty_@3, eg), eh), fa)) → new_esEs3(xv300, xv4000, eg, eh, fa)
new_esEs2(:(xv300, xv301), :(xv4000, xv4001), app(app(ty_Either, ff), fg)) → new_esEs1(xv300, xv4000, ff, fg)
new_esEs2(:(xv300, xv301), :(xv4000, xv4001), gd) → new_esEs2(xv301, xv4001, gd)
new_esEs3(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), hh, app(ty_[], baf), gh) → new_esEs2(xv301, xv4001, baf)
new_esEs2(:(xv300, xv301), :(xv4000, xv4001), app(app(ty_@2, fb), fc)) → new_esEs(xv300, xv4000, fb, fc)
new_esEs(@2(Left(xv300), xv31), @2(Left(xv4000), xv401), app(app(ty_Either, app(ty_Maybe, da)), cg), bc) → new_esEs0(xv300, xv4000, da)
new_esEs(@2(Just(xv300), xv31), @2(Just(xv4000), xv401), app(ty_Maybe, app(ty_[], ca)), bc) → new_esEs2(xv300, xv4000, ca)
new_esEs(@2(Right(xv300), xv31), @2(Right(xv4000), xv401), app(app(ty_Either, dh), app(ty_[], ef)), bc) → new_esEs2(xv300, xv4000, ef)
new_esEs3(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), hh, gg, app(app(ty_Either, bbe), bbf)) → new_esEs1(xv302, xv4002, bbe, bbf)
new_esEs(@2(Right(xv300), xv31), @2(Right(xv4000), xv401), app(app(ty_Either, dh), app(app(app(ty_@3, eg), eh), fa)), bc) → new_esEs3(xv300, xv4000, eg, eh, fa)
new_esEs(@2(:(xv300, xv301), xv31), @2(:(xv4000, xv4001), xv401), app(ty_[], app(ty_[], fh)), bc) → new_esEs2(xv300, xv4000, fh)
new_esEs1(Right(xv300), Right(xv4000), dh, app(ty_[], ef)) → new_esEs2(xv300, xv4000, ef)
new_esEs2(:(xv300, xv301), :(xv4000, xv4001), app(app(app(ty_@3, ga), gb), gc)) → new_esEs3(xv300, xv4000, ga, gb, gc)
new_esEs1(Left(xv300), Left(xv4000), app(app(app(ty_@3, de), df), dg), cg) → new_esEs3(xv300, xv4000, de, df, dg)
new_esEs3(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), app(app(app(ty_@3, he), hf), hg), gg, gh) → new_esEs3(xv300, xv4000, he, hf, hg)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_esEs0(Just(xv300), Just(xv4000), app(app(ty_@2, bd), be)) → new_esEs(xv300, xv4000, bd, be)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs0(Just(xv300), Just(xv4000), app(app(app(ty_@3, cb), cc), cd)) → new_esEs3(xv300, xv4000, cb, cc, cd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs0(Just(xv300), Just(xv4000), app(app(ty_Either, bg), bh)) → new_esEs1(xv300, xv4000, bg, bh)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs2(:(xv300, xv301), :(xv4000, xv4001), app(app(ty_@2, fb), fc)) → new_esEs(xv300, xv4000, fb, fc)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs2(:(xv300, xv301), :(xv4000, xv4001), app(app(app(ty_@3, ga), gb), gc)) → new_esEs3(xv300, xv4000, ga, gb, gc)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs2(:(xv300, xv301), :(xv4000, xv4001), app(app(ty_Either, ff), fg)) → new_esEs1(xv300, xv4000, ff, fg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs0(Just(xv300), Just(xv4000), app(ty_Maybe, bf)) → new_esEs0(xv300, xv4000, bf)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs0(Just(xv300), Just(xv4000), app(ty_[], ca)) → new_esEs2(xv300, xv4000, ca)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs2(:(xv300, xv301), :(xv4000, xv4001), app(ty_Maybe, fd)) → new_esEs0(xv300, xv4000, fd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs(@2(xv30, xv31), @2(xv400, xv401), app(app(ty_@2, ba), bb), bc) → new_esEs(xv30, xv400, ba, bb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs(@2(@3(xv300, xv301, xv302), xv31), @2(@3(xv4000, xv4001, xv4002), xv401), app(app(app(ty_@3, app(app(ty_@2, ge), gf)), gg), gh), bc) → new_esEs(xv300, xv4000, ge, gf)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs(@2(Just(xv300), xv31), @2(Just(xv4000), xv401), app(ty_Maybe, app(app(ty_@2, bd), be)), bc) → new_esEs(xv300, xv4000, bd, be)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs(@2(Right(xv300), xv31), @2(Right(xv4000), xv401), app(app(ty_Either, dh), app(app(ty_@2, ea), eb)), bc) → new_esEs(xv300, xv4000, ea, eb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs(@2(xv30, xv31), @2(xv400, xv401), bcc, app(app(ty_@2, bcd), bce)) → new_esEs(xv31, xv401, bcd, bce)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs(@2(Left(xv300), xv31), @2(Left(xv4000), xv401), app(app(ty_Either, app(app(ty_@2, ce), cf)), cg), bc) → new_esEs(xv300, xv4000, ce, cf)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs(@2(@3(xv300, xv301, xv302), xv31), @2(@3(xv4000, xv4001, xv4002), xv401), app(app(app(ty_@3, hh), app(app(ty_@2, baa), bab)), gh), bc) → new_esEs(xv301, xv4001, baa, bab)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs(@2(@3(xv300, xv301, xv302), xv31), @2(@3(xv4000, xv4001, xv4002), xv401), app(app(app(ty_@3, hh), gg), app(app(ty_@2, bbb), bbc)), bc) → new_esEs(xv302, xv4002, bbb, bbc)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs(@2(:(xv300, xv301), xv31), @2(:(xv4000, xv4001), xv401), app(ty_[], app(app(ty_@2, fb), fc)), bc) → new_esEs(xv300, xv4000, fb, fc)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs(@2(@3(xv300, xv301, xv302), xv31), @2(@3(xv4000, xv4001, xv4002), xv401), app(app(app(ty_@3, hh), gg), app(app(app(ty_@3, bbh), bca), bcb)), bc) → new_esEs3(xv302, xv4002, bbh, bca, bcb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs(@2(@3(xv300, xv301, xv302), xv31), @2(@3(xv4000, xv4001, xv4002), xv401), app(app(app(ty_@3, app(app(app(ty_@3, he), hf), hg)), gg), gh), bc) → new_esEs3(xv300, xv4000, he, hf, hg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs(@2(@3(xv300, xv301, xv302), xv31), @2(@3(xv4000, xv4001, xv4002), xv401), app(app(app(ty_@3, hh), app(app(app(ty_@3, bag), bah), bba)), gh), bc) → new_esEs3(xv301, xv4001, bag, bah, bba)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs(@2(xv30, xv31), @2(xv400, xv401), bcc, app(app(app(ty_@3, bdb), bdc), bdd)) → new_esEs3(xv31, xv401, bdb, bdc, bdd)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4, 4 > 5
- new_esEs(@2(:(xv300, xv301), xv31), @2(:(xv4000, xv4001), xv401), app(ty_[], app(app(app(ty_@3, ga), gb), gc)), bc) → new_esEs3(xv300, xv4000, ga, gb, gc)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs(@2(Just(xv300), xv31), @2(Just(xv4000), xv401), app(ty_Maybe, app(app(app(ty_@3, cb), cc), cd)), bc) → new_esEs3(xv300, xv4000, cb, cc, cd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs(@2(Left(xv300), xv31), @2(Left(xv4000), xv401), app(app(ty_Either, app(app(app(ty_@3, de), df), dg)), cg), bc) → new_esEs3(xv300, xv4000, de, df, dg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs(@2(Right(xv300), xv31), @2(Right(xv4000), xv401), app(app(ty_Either, dh), app(app(app(ty_@3, eg), eh), fa)), bc) → new_esEs3(xv300, xv4000, eg, eh, fa)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs(@2(@3(xv300, xv301, xv302), xv31), @2(@3(xv4000, xv4001, xv4002), xv401), app(app(app(ty_@3, app(app(ty_Either, hb), hc)), gg), gh), bc) → new_esEs1(xv300, xv4000, hb, hc)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs(@2(@3(xv300, xv301, xv302), xv31), @2(@3(xv4000, xv4001, xv4002), xv401), app(app(app(ty_@3, hh), app(app(ty_Either, bad), bae)), gh), bc) → new_esEs1(xv301, xv4001, bad, bae)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs(@2(Right(xv300), xv31), @2(Right(xv4000), xv401), app(app(ty_Either, dh), app(app(ty_Either, ed), ee)), bc) → new_esEs1(xv300, xv4000, ed, ee)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs(@2(xv30, xv31), @2(xv400, xv401), bcc, app(app(ty_Either, bcg), bch)) → new_esEs1(xv31, xv401, bcg, bch)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs(@2(@3(xv300, xv301, xv302), xv31), @2(@3(xv4000, xv4001, xv4002), xv401), app(app(app(ty_@3, hh), gg), app(app(ty_Either, bbe), bbf)), bc) → new_esEs1(xv302, xv4002, bbe, bbf)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs(@2(:(xv300, xv301), xv31), @2(:(xv4000, xv4001), xv401), app(ty_[], app(app(ty_Either, ff), fg)), bc) → new_esEs1(xv300, xv4000, ff, fg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs(@2(Just(xv300), xv31), @2(Just(xv4000), xv401), app(ty_Maybe, app(app(ty_Either, bg), bh)), bc) → new_esEs1(xv300, xv4000, bg, bh)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs(@2(Left(xv300), xv31), @2(Left(xv4000), xv401), app(app(ty_Either, app(app(ty_Either, db), dc)), cg), bc) → new_esEs1(xv300, xv4000, db, dc)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs(@2(@3(xv300, xv301, xv302), xv31), @2(@3(xv4000, xv4001, xv4002), xv401), app(app(app(ty_@3, hh), gg), app(ty_Maybe, bbd)), bc) → new_esEs0(xv302, xv4002, bbd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs(@2(:(xv300, xv301), xv31), @2(:(xv4000, xv4001), xv401), app(ty_[], app(ty_Maybe, fd)), bc) → new_esEs0(xv300, xv4000, fd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs(@2(Right(xv300), xv31), @2(Right(xv4000), xv401), app(app(ty_Either, dh), app(ty_Maybe, ec)), bc) → new_esEs0(xv300, xv4000, ec)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs(@2(@3(xv300, xv301, xv302), xv31), @2(@3(xv4000, xv4001, xv4002), xv401), app(app(app(ty_@3, hh), app(ty_Maybe, bac)), gh), bc) → new_esEs0(xv301, xv4001, bac)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs(@2(@3(xv300, xv301, xv302), xv31), @2(@3(xv4000, xv4001, xv4002), xv401), app(app(app(ty_@3, app(ty_Maybe, ha)), gg), gh), bc) → new_esEs0(xv300, xv4000, ha)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs(@2(xv30, xv31), @2(xv400, xv401), bcc, app(ty_Maybe, bcf)) → new_esEs0(xv31, xv401, bcf)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs(@2(Just(xv300), xv31), @2(Just(xv4000), xv401), app(ty_Maybe, app(ty_Maybe, bf)), bc) → new_esEs0(xv300, xv4000, bf)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs(@2(Left(xv300), xv31), @2(Left(xv4000), xv401), app(app(ty_Either, app(ty_Maybe, da)), cg), bc) → new_esEs0(xv300, xv4000, da)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs(@2(xv30, xv31), @2(xv400, xv401), bcc, app(ty_[], bda)) → new_esEs2(xv31, xv401, bda)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs(@2(@3(xv300, xv301, xv302), xv31), @2(@3(xv4000, xv4001, xv4002), xv401), app(app(app(ty_@3, app(ty_[], hd)), gg), gh), bc) → new_esEs2(xv300, xv4000, hd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs(@2(@3(xv300, xv301, xv302), xv31), @2(@3(xv4000, xv4001, xv4002), xv401), app(app(app(ty_@3, hh), app(ty_[], baf)), gh), bc) → new_esEs2(xv301, xv4001, baf)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs(@2(@3(xv300, xv301, xv302), xv31), @2(@3(xv4000, xv4001, xv4002), xv401), app(app(app(ty_@3, hh), gg), app(ty_[], bbg)), bc) → new_esEs2(xv302, xv4002, bbg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs(@2(Left(xv300), xv31), @2(Left(xv4000), xv401), app(app(ty_Either, app(ty_[], dd)), cg), bc) → new_esEs2(xv300, xv4000, dd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs(@2(:(xv300, xv301), xv31), @2(:(xv4000, xv4001), xv401), app(ty_[], gd), bc) → new_esEs2(xv301, xv4001, gd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs(@2(Right(xv300), xv31), @2(Right(xv4000), xv401), app(app(ty_Either, dh), app(ty_[], ef)), bc) → new_esEs2(xv300, xv4000, ef)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs(@2(Just(xv300), xv31), @2(Just(xv4000), xv401), app(ty_Maybe, app(ty_[], ca)), bc) → new_esEs2(xv300, xv4000, ca)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs(@2(:(xv300, xv301), xv31), @2(:(xv4000, xv4001), xv401), app(ty_[], app(ty_[], fh)), bc) → new_esEs2(xv300, xv4000, fh)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs1(Right(xv300), Right(xv4000), dh, app(app(ty_@2, ea), eb)) → new_esEs(xv300, xv4000, ea, eb)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs1(Left(xv300), Left(xv4000), app(app(ty_@2, ce), cf), cg) → new_esEs(xv300, xv4000, ce, cf)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs3(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), hh, gg, app(app(ty_@2, bbb), bbc)) → new_esEs(xv302, xv4002, bbb, bbc)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4
- new_esEs3(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), hh, app(app(ty_@2, baa), bab), gh) → new_esEs(xv301, xv4001, baa, bab)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs3(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), app(app(ty_@2, ge), gf), gg, gh) → new_esEs(xv300, xv4000, ge, gf)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs1(Right(xv300), Right(xv4000), dh, app(app(app(ty_@3, eg), eh), fa)) → new_esEs3(xv300, xv4000, eg, eh, fa)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4, 4 > 5
- new_esEs1(Left(xv300), Left(xv4000), app(app(app(ty_@3, de), df), dg), cg) → new_esEs3(xv300, xv4000, de, df, dg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs1(Left(xv300), Left(xv4000), app(app(ty_Either, db), dc), cg) → new_esEs1(xv300, xv4000, db, dc)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs1(Right(xv300), Right(xv4000), dh, app(app(ty_Either, ed), ee)) → new_esEs1(xv300, xv4000, ed, ee)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs1(Right(xv300), Right(xv4000), dh, app(ty_Maybe, ec)) → new_esEs0(xv300, xv4000, ec)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs1(Left(xv300), Left(xv4000), app(ty_Maybe, da), cg) → new_esEs0(xv300, xv4000, da)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs1(Left(xv300), Left(xv4000), app(ty_[], dd), cg) → new_esEs2(xv300, xv4000, dd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs1(Right(xv300), Right(xv4000), dh, app(ty_[], ef)) → new_esEs2(xv300, xv4000, ef)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs3(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), hh, gg, app(app(app(ty_@3, bbh), bca), bcb)) → new_esEs3(xv302, xv4002, bbh, bca, bcb)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4, 5 > 5
- new_esEs3(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), hh, app(app(app(ty_@3, bag), bah), bba), gh) → new_esEs3(xv301, xv4001, bag, bah, bba)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4, 4 > 5
- new_esEs3(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), app(app(app(ty_@3, he), hf), hg), gg, gh) → new_esEs3(xv300, xv4000, he, hf, hg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs3(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), app(app(ty_Either, hb), hc), gg, gh) → new_esEs1(xv300, xv4000, hb, hc)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs3(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), hh, app(app(ty_Either, bad), bae), gh) → new_esEs1(xv301, xv4001, bad, bae)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs3(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), hh, gg, app(app(ty_Either, bbe), bbf)) → new_esEs1(xv302, xv4002, bbe, bbf)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4
- new_esEs2(:(xv300, xv301), :(xv4000, xv4001), app(ty_[], fh)) → new_esEs2(xv300, xv4000, fh)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs2(:(xv300, xv301), :(xv4000, xv4001), gd) → new_esEs2(xv301, xv4001, gd)
The graph contains the following edges 1 > 1, 2 > 2, 3 >= 3
- new_esEs3(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), hh, app(ty_Maybe, bac), gh) → new_esEs0(xv301, xv4001, bac)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs3(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), hh, gg, app(ty_Maybe, bbd)) → new_esEs0(xv302, xv4002, bbd)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3
- new_esEs3(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), app(ty_Maybe, ha), gg, gh) → new_esEs0(xv300, xv4000, ha)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs3(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), app(ty_[], hd), gg, gh) → new_esEs2(xv300, xv4000, hd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs3(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), hh, gg, app(ty_[], bbg)) → new_esEs2(xv302, xv4002, bbg)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3
- new_esEs3(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), hh, app(ty_[], baf), gh) → new_esEs2(xv301, xv4001, baf)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
Q DP problem:
The TRS P consists of the following rules:
new_foldr(xv3, :(xv40, xv41), ba, bb) → new_foldr(xv3, xv41, ba, bb)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_foldr(xv3, :(xv40, xv41), ba, bb) → new_foldr(xv3, xv41, ba, bb)
The graph contains the following edges 1 >= 1, 2 > 2, 3 >= 3, 4 >= 4